Nuprl Lemma : ma-atom-free
0,22
postcript
pdf
AtomFree(Type{i'};msga{i:l})
latex
Definitions
AtomFree(
T
;
x
)
,
a
:
A
fp
B
(
a
)
,
Id
,
Type
,
x
:
A
B
(
x
)
,
MsgA
Lemmas
msga
wf
origin
B(a)
B(x) B(a)B(x)